Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		app(f,0)	→ true
2:		app(f,1)	→ false
3:		app(f,app(s,x))	→ app(f,x)
4:		app(app(app(if,true),app(s,x)),app(s,y))	→ app(s,x)
5:		app(app(app(if,false),app(s,x)),app(s,y))	→ app(s,y)
6:		app(app(g,x),app(c,y))	→ app(c,app(app(g,x),y))
7:		app(app(g,x),app(c,y))	→ app(app(g,x),app(app(app(if,app(f,x)),app(c,app(app(g,app(s,x)),y))),app(c,y)))

There are 12 dependency pairs:


8:		APP(f,app(s,x))	→ APP(f,x)
9:		APP(app(g,x),app(c,y))	→ APP(c,app(app(g,x),y))
10:		APP(app(g,x),app(c,y))	→ APP(app(g,x),y)
11:		APP(app(g,x),app(c,y))	→ APP(app(g,x),app(app(app(if,app(f,x)),app(c,app(app(g,app(s,x)),y))),app(c,y)))
12:		APP(app(g,x),app(c,y))	→ APP(app(app(if,app(f,x)),app(c,app(app(g,app(s,x)),y))),app(c,y))
13:		APP(app(g,x),app(c,y))	→ APP(app(if,app(f,x)),app(c,app(app(g,app(s,x)),y)))
14:		APP(app(g,x),app(c,y))	→ APP(if,app(f,x))
15:		APP(app(g,x),app(c,y))	→ APP(f,x)
16:		APP(app(g,x),app(c,y))	→ APP(c,app(app(g,app(s,x)),y))
17:		APP(app(g,x),app(c,y))	→ APP(app(g,app(s,x)),y)
18:		APP(app(g,x),app(c,y))	→ APP(g,app(s,x))
19:		APP(app(g,x),app(c,y))	→ APP(s,x)

The approximated dependency graph contains 2 SCCs: {8} and {10-13,17}.

Consider the SCC {8}. There are no usable rules. By taking the AF π with π(APP) = 2 and π(app) = [2] together with the lexicographic path order with empty precedence, rule 8 is strictly decreasing.

Consider the SCC {10-13,17}. By taking the AF π with π(app) = π(APP) = 1 together with the lexicographic path order with precedence f ≻ false, f ≻ true, g ≻ c and g ≻ if ≻ s, the rules in {3,7,10,11,17} are weakly decreasing and the rules in {1,2,4-6,12,13} are strictly decreasing. There is one new SCC.
- Consider the SCC {10,11,17}. The constraints could not be solved.

Tyrolean Termination Tool (3.57 seconds) --- May 4, 2006